a(l(x1)) → l(a(x1))
r(a(x1)) → a(r(x1))
b(l(x1)) → b(a(r(x1)))
r(b(x1)) → l(b(x1))
↳ QTRS
↳ DependencyPairsProof
a(l(x1)) → l(a(x1))
r(a(x1)) → a(r(x1))
b(l(x1)) → b(a(r(x1)))
r(b(x1)) → l(b(x1))
B(l(x1)) → A(r(x1))
B(l(x1)) → R(x1)
R(a(x1)) → R(x1)
R(a(x1)) → A(r(x1))
B(l(x1)) → B(a(r(x1)))
A(l(x1)) → A(x1)
a(l(x1)) → l(a(x1))
r(a(x1)) → a(r(x1))
b(l(x1)) → b(a(r(x1)))
r(b(x1)) → l(b(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
B(l(x1)) → A(r(x1))
B(l(x1)) → R(x1)
R(a(x1)) → R(x1)
R(a(x1)) → A(r(x1))
B(l(x1)) → B(a(r(x1)))
A(l(x1)) → A(x1)
a(l(x1)) → l(a(x1))
r(a(x1)) → a(r(x1))
b(l(x1)) → b(a(r(x1)))
r(b(x1)) → l(b(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
A(l(x1)) → A(x1)
a(l(x1)) → l(a(x1))
r(a(x1)) → a(r(x1))
b(l(x1)) → b(a(r(x1)))
r(b(x1)) → l(b(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
A(l(x1)) → A(x1)
The value of delta used in the strict ordering is 4.
POL(l(x1)) = 1 + (4)x_1
POL(A(x1)) = (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
a(l(x1)) → l(a(x1))
r(a(x1)) → a(r(x1))
b(l(x1)) → b(a(r(x1)))
r(b(x1)) → l(b(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
R(a(x1)) → R(x1)
a(l(x1)) → l(a(x1))
r(a(x1)) → a(r(x1))
b(l(x1)) → b(a(r(x1)))
r(b(x1)) → l(b(x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
R(a(x1)) → R(x1)
The value of delta used in the strict ordering is 4.
POL(a(x1)) = 1 + (4)x_1
POL(R(x1)) = (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
a(l(x1)) → l(a(x1))
r(a(x1)) → a(r(x1))
b(l(x1)) → b(a(r(x1)))
r(b(x1)) → l(b(x1))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
B(l(x1)) → B(a(r(x1)))
a(l(x1)) → l(a(x1))
r(a(x1)) → a(r(x1))
b(l(x1)) → b(a(r(x1)))
r(b(x1)) → l(b(x1))